/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.transform;

import java.util.HashMap;
import java.util.Map;

import alloy.ast.Formula;
import alloy.ast.InvocablePara;
import alloy.ast.InvocationFormula;


/** We will not deal with this for now -- most of the old code is commented out. **/

/**
  Contains methods for <em>skolemizing</em> functions, ie. creating a relation
  which contains tuples corresponding to argument values for which the function body
  is true.  Skolemizing a function involves the following steps:
  <ul>
  <li>Create a global relation for the function.  The relation will have the
  same name as the function.
  <li>Constrain the new relation appropriately by adding a new global fact.  See
  recursion.txt in the doc/ directory for details.
  <li>Replace the body of the skolemized function appropriately.
  </ul>
  Note that for now, only functions with all scalar arguments can be skolemized.
*/

public class FunctionSkolemizer implements alloy.util.AlloyConstants {

    /** name of field added to wrapper sigs */
    private static final String FIELD_NAME = "f";

    /**
       Map from Functions which have been skolemized to an
       expression representing the new relation
    */
    private Map _funToRel = new HashMap(); // Map[Function -> Expr]

    /**
       Map from Signatures to wrapping Signature, if one
       has been created
    */
    private Map _sigToWrapper = new HashMap();  // Map[Signature -> Signature]

    /**
       For functions which have non-scalar args, map from
       function to set of indices of arguments which need
       wrapping on invocations
    */
    private Map _funToWrapIndices = new HashMap(); // Map[Function -> Set[Integer]]

    /**
       Skolemize a function.  This involves creating a new relation representing
       the function, adding a fact which constrains the function, and changing the
       body of the function.
    */
    public void skolemizeFunction(InvocablePara invocable_) {
    /**
        _createRelation(invocable_);
        _addRelationFact(invocable_);
    **/
    }

    /**
       @return <code>true</code> if function_ has been skolemized; <code>false</code>
       otherwise
    */
    public boolean isSkolemized(InvocablePara function_) {
        return _funToRel.containsKey(function_);
    }

    /**
       Inline an invocation of a skolemized function.  If a function foo has been skolemized,
       then an invocation <code>foo(x,y,z,...)</code> will be transformed to
       <code>x -> y -> z -> ... in foo</code>.
    */
    public Formula inlineSkolemized(InvocationFormula invFormula_) {
    /**
        InvocablePara invokedFun = invFormula_.getInvocable();
        Dbg.chk(_funToRel.containsKey(invokedFun));
        Expr relExpr = (Expr)((Expr)_funToRel.get(invokedFun)).copy();
        if (!_funToWrapIndices.containsKey(invokedFun)) {
            return _simpleInlineSkolemized(invFormula_, relExpr);
        } else {
            return _inlineSkolemizedWithWrappers(invFormula_, invokedFun, relExpr);
        }
    **/
    throw new RuntimeException("We cannot deal with skolemization yet");
    }

    /**
    private Formula _simpleInlineSkolemized(InvocationFormula invFormula_,
                                            Expr relExpr_) {
        // construct tuple out of args
        Expr tupleExpr = null;
        Iterator argIter = invFormula_.getArgs().iterator();
        while (argIter.hasNext()) {
            Expr curArg = (Expr)((Expr)argIter.next()).copy();
            if (tupleExpr == null) {
                tupleExpr = curArg;
            } else {
                tupleExpr = tupleExpr.product(curArg);
            }
        }
        return tupleExpr.in(relExpr_);
    }
    **/

    /**
    private Formula _inlineSkolemizedWithWrappers(InvocationFormula invFormula_,
                                                  InvocablePara invokedFun_,
                                                  Expr relExpr_) {
        // construct tuple out of args, wrapping with comprehension
        // expressions when necessary
        Expr tupleExpr = null;
        Iterator argIter = invFormula_.getArgs().iterator();
        int argIndex = 0;
        while (argIter.hasNext()) {
            Expr curArg = (Expr)((Expr)argIter.next()).copy();
            Expr tupleAddition = curArg;
            if (_needsWrapper(invokedFun_, argIndex)) {
                // see if argument has already been wrapped and is being passed unmodified
                // recursively
                if (_usesWrapper(curArg)) {
                    tupleAddition = (Expr)((BinaryExpr)curArg).getLeft().copy();
                } else {
                    // create comprehension expression
                    // { wr : W | wr.f = arg }
                    SetMultExpr wrapperMultExpr = _wrapperSigSetMultExpr((SigType)curArg.getType().getBasicTypeAt(0));
                    Variable wrapperVar = new Variable(Id.generateId("wr"));
                    Decl decl = Decl.in(wrapperVar, wrapperMultExpr);
                    Decls decls = new Decls();
                    decls.addDecl(decl);
                    // create an expression which should replace the wrapped arg
                    Expr wrapVarExpr = new VariableExpr((Variable)wrapperVar.copy());
                    wrapVarExpr.setType(wrapperMultExpr.getType());
                    Expr fieldExpr = new VariableExpr(new Variable(new Id(FIELD_NAME)));
                    RelationType fieldType = RelationType.append(wrapperMultExpr.getType(),
                                                                 curArg.getType());
                    fieldExpr.setType(fieldType);
                    Expr joinExpr = wrapVarExpr.join(fieldExpr);
                    Formula compBody = joinExpr.eq(curArg);
                    Expr compExpr = new ComprehensionExpr(decls, compBody, true);
                    compExpr.setType(wrapVarExpr.getType());
                    tupleAddition = compExpr;
                }
            }
            if (tupleExpr == null) {
                tupleExpr = tupleAddition;
            } else {
                tupleExpr = tupleExpr.product(tupleAddition);
            }
            argIndex++;
        }
        return tupleExpr.in(relExpr_);
    }
    **/

    /**
       @return <code>true</code> if expr_ is of the form <code>e.f</code>,
       where <code>e</code> has the type of a wrapper and <code>f</code> is its
       field
    */
    /**
    private boolean _usesWrapper(Expr expr_) {
        if (expr_ instanceof BinaryExpr) {
            BinaryExpr binExpr = (BinaryExpr)expr_;
            if (binExpr.getOp().getOpCode() == BinaryExprOp.JOIN_DOT) {
                Expr left = binExpr.getLeft();
                Expr right = binExpr.getRight();
                if (left instanceof VariableExpr &&
                    right instanceof VariableExpr) {
                    RelationType leftType = left.getType();
                    RelationType rightType = right.getType();
                    if (leftType.numBasicTypes() == 1 &&
                        rightType.numBasicTypes() == 2) {
                        BasicType basType = leftType.getBasicTypeAt(0);
                        if (basType instanceof SigType &&
                            ((SigType)basType).getSignature().wrappedSig != null) {
                            return true;
                        }
                    }
                }
            }
        }
        return false;
    }
    **/

    /**
    private void _createRelation(InvocablePara function_) {
        // NOTE: i don't think this will cause name clash issues (since paragraph
        // names cannot be shadowed), but not 100% sure
        String relationName = function_.getName().toString();
        // first, create leaf id for skolemized function
        LeafId funLeafId = new LeafId();
        RelationType relType = new RelationType();
        InOrderFormalIter formalIter = function_.getArgList().orderedIter();
        int argIndex = 0;
        Dbg.chk(formalIter.hasNext());
        while (formalIter.hasNext()) {
            // don't care about formal, only decl
            formalIter.next();
            Decl curDecl = formalIter.getCurDecl();
            SetMultExpr multExpr = (SetMultExpr)curDecl.getExpr();
            RelationType curDeclType = multExpr.getType();
            RelationType appendType = curDeclType;
            int multOpCode = multExpr.getSetMult().getOpCode();
            if (multOpCode == SetMultiplicity.OPTION ||
                multOpCode == SetMultiplicity.SET) {
                // need a wrapper
                appendType = _createWrapperType(curDeclType, multOpCode);
                // add this argument index as one which needs wrapping
                // on invocations
                _addWrapIndex(function_, argIndex);
            }
            relType = RelationType.append(relType, appendType);
            argIndex++;
        }
        // create expression representing new relation
        VariableExpr relExpr = new VariableExpr(new Variable(new Id(relationName)));
        relExpr.setType(relType);
        relExpr.setLeafId(funLeafId);
        _funToRel.put(function_, relExpr);
    }
    **/
    /**
    private RelationType _createWrapperType(RelationType wrappedType_,
                                            int multOpCode_) {
        // get signature
        // we know wrappedType_ has one basic type which is a SigType
        SigType sigType = (SigType)wrappedType_.getBasicTypeAt(0);
        Signature sig = sigType.getSignature();
        // see if sig has already been wrapped
        if (_sigToWrapper.containsKey(sig)) {
            Signature wrapperSig = (Signature)_sigToWrapper.get(sig);
            // if current multiplicity is set, change wrapOption of
            // wrapperSig to false
            if (multOpCode_ == SetMultiplicity.SET) {
                _makeFieldSetMult(wrapperSig);
            }
            return new RelationType(wrapperSig.getSigType());
        }
        // need to create new wrapper sig

        // first, create new Signature
        QualifiedName wrapperName = new QualifiedName(Id.generateId(WRAPSIG_PREFIX + "_" + sig.getName().getId().nodeString()),
                                                      (Path)sig.getName().getPath().copy());
        Signature wrapperSig = new Signature(wrapperName);

        // add to module scope
        ModuleInfo moduleInfo = ((Module)sig.getParent().getParent()).getModuleInfo();
        try {
            moduleInfo.addOpenedParagraph(wrapperSig.getName(), wrapperSig);
        } catch (AlreadyMappedException ame) {
            Dbg.fatal("shouldn't happen");
        }

        // create new SigType
    Dbg.chk(!SigType.hasSigType(wrapperSig));
        SigType wrapperType = SigType.getGlobalSigType(wrapperSig, null);

        wrapperSig.setSigType(wrapperType);

        // create declaration of field
        // let's be creative and call it "f" :-)
        Variable var = new Variable(new Id(FIELD_NAME));
        // always use SET multiplicity, so no constraints are generated
        // optimization will take care of actual multiplicity
        SetMultExpr multExpr = new SetMultExpr(new SetMultiplicity(multOpCode_),
                                               sigType.toSigExpr());
        multExpr.setType(wrappedType_);
        Decl decl = Decl.in(var, multExpr);
        Decls decls = new Decls();
        decls.addDecl(decl);

        wrapperSig.setDecls(decls);

        // flag wrapperSig as a wrapper, and as a product sig
        wrapperSig.wrappedSig = sig;
        wrapperSig.setProduct(true);

        // add to mapping
        _sigToWrapper.put(sig, wrapperSig);

        // set the LocalScope of wrappedSig
        LocalScope fieldLocalScope = new LocalScope();
        try {
            fieldLocalScope.addMapping(var.nodeString(), RelationType.append(new RelationType(wrapperType),
                                                                             wrappedType_));
        } catch (AlreadyMappedException ame) {
            Dbg.fatal("shouldn't happen");
        }
        LocalScope typeParamLocalScope = new LocalScope();
        typeParamLocalScope.addParent(fieldLocalScope);
        wrapperSig.setLocalScope(typeParamLocalScope);

        // the leaf id for the field f should be allocated by ImplicitConstraintGenerator later
        return new RelationType(wrapperType);
    }
    **/

    /**
    private void _addWrapIndex(InvocablePara function_, int index_) {
        if (_funToWrapIndices.containsKey(function_)) {
            ((Set)_funToWrapIndices.get(function_)).add(new Integer(index_));
        } else {
            Set indexSet = new HashSet();
            indexSet.add(new Integer(index_));
            _funToWrapIndices.put(function_, indexSet);
        }
    }

    private void _makeFieldSetMult(Signature wrapperSig_) {
        Decl fieldDecl = (Decl)wrapperSig_.getDecls().getDeclIter().next();
        SetMultExpr setMultExpr = (SetMultExpr)fieldDecl.getExpr();
        fieldDecl.setExpr(new SetMultExpr(new SetMultiplicity(SetMultiplicity.SET),
                                          setMultExpr.getExpr()));
    }
    **/

    /**
       For a function foo(b : B), where B has type A,
       we generate the formula
       foo in A && all b : A | b in foo <=> b in B && body of foo

       We need the "b in B" part of the constraint since argument
       declarations can constrain arguments based on previous
       arguments, eg. foo(b : B, c : b).

       A later inlining phase will handle the invocation
       of foo appropriately.
    */

    /**
    private void _addRelationFact(InvocablePara function_) {
        // construct useful syntax for constraints

        // VariableExprs corresponding to the *actual* formal
        // names, but not necessarily the variables in the
        // created quantified formula
        // useful for desugaring recursive function body
        Exprs varExprs = new Exprs();
        // declarations to be used in quantified formula...
        // might include declarations over wrapper signatures
        // instead of signatures in decls of formals
        Decls decls = new Decls();
        // an expression representing the set of tuples which
        // each tuple must belong to
        // we need this because of formal decls which use
        // earlier formals
        Expr setExpr = null;
        // represents the current tuple being constrained in
        // the quantifier
        Expr curTupleExpr = null;
        // a mapping from String variable names to replacement
        // expressions for wrapped args
        Map varExprMapping = new HashMap();
        InOrderFormalIter formalIter = function_.getArgList().orderedIter();
        int argIndex = 0;
        while (formalIter.hasNext()) {
            Variable curVar = formalIter.nextVar();
            Decl curDecl = formalIter.getCurDecl();
            SetMultExpr multExpr = (SetMultExpr)curDecl.getExpr();
            RelationType type = multExpr.getType();
            VariableExpr varExpr = new VariableExpr((Variable)curVar.copy());
            varExpr.setType(type);
            varExprs.addExpr(varExpr);
            Variables vars = new Variables();
            SetMultExpr sme = null;
            Expr tupleAddition = null;
            if (_needsWrapper(function_, argIndex)) {
                // create a variable for wrapper sig
                Variable wrapperVar = new Variable(Id.generateId("wrap_" + curVar.nodeString()));
                vars.addVariable(wrapperVar);
                // create RHS of decl
                sme = _wrapperSigSetMultExpr((SigType)type.getBasicTypeAt(0));
                // create an expression which should replace the wrapped arg
                Expr wrapVarExpr = new VariableExpr((Variable)wrapperVar.copy());
                wrapVarExpr.setType(sme.getType());
                Expr fieldExpr = new VariableExpr(new Variable(new Id(FIELD_NAME)));
                RelationType fieldType = RelationType.append(sme.getType(), type);
                fieldExpr.setType(fieldType);
                Expr replacementExpr = wrapVarExpr.join(fieldExpr);
                // add to mappoing
                varExprMapping.put(curVar.nodeString(), replacementExpr);
                tupleAddition = wrapVarExpr;
            } else {
                vars.addVariable((Variable)curVar.copy());
                sme = new SetMultExpr(new SetMultiplicity(SetMultiplicity.NONE),
                                      type.toExpr());
                sme.setType(type);
                tupleAddition = varExpr;
            }
            if (curTupleExpr == null)
                curTupleExpr = tupleAddition;
            else
                curTupleExpr = curTupleExpr.product(tupleAddition);
            Decl varDecl = new Decl(new Qualifiers(), vars,
                                    (CompOp)curDecl.getOp().copy(),
                                    sme);
            decls.addDecl(varDecl);
            Expr curSetExpr = (Expr)multExpr.getExpr().copy();
            if (setExpr == null)
                setExpr = curSetExpr;
            else
                setExpr = setExpr.product(curSetExpr);
            argIndex++;
        } // while (formalIter.hasNext())

        // create "b in foo"
        Expr relExpr = (Expr)((Expr)_funToRel.get(function_)).copy();
        Formula lhs = curTupleExpr.in(relExpr);
        // create "b in B"
        Iterator exprIter = varExprs.getExprIter();
        Expr argTupleExpr = (Expr)((Expr)exprIter.next()).copy();
        while (exprIter.hasNext()) {
            argTupleExpr = argTupleExpr.product((Expr)((Expr)exprIter.next()).copy());
        }
        Formula setConstraint = argTupleExpr.in(setExpr);
        // copy function body
        Formula bodyCopy = (Formula)function_.getFormula().copy();
        Formula rhs = setConstraint.and(bodyCopy);
        // replace original formals with wrappers
        rhs = (Formula)rhs.applyReturnVisitor(new ExprAndTypeReplaceVisitor(varExprMapping, new HashMap(),
                                                                            "wrapped formals", "wrapper expressions",
                                                                            Collections.EMPTY_SET));
        // create body of quantifier
        Formula quantBody = lhs.iff(rhs);
        // create quantifier
        Formula constraint = new QuantifiedFormula(Quantifier.ALL,
                                                   decls, quantBody, true);

        // also need to say that global relation is within types
        constraint = ((Expr)relExpr.copy()).in(relExpr.getType().toExpr()).and(constraint);

        // create fact
        Id id = Id.generateId(function_.getName().getId().nodeString() + "_fact");
        QualifiedName factName = new QualifiedName(id, (Path)function_.getName().getPath().copy());
        FormulaSeq factBody = new FormulaSeq(constraint);
        Fact fact = new Fact(factName, new Ids(), factBody);
        // add fact to function's module
        Module module = (Module)function_.getParent().getParent();
        module.getFacts().addFact(fact);

        // also, replace the body of the function with an invocation to itself
        // seems weird, but inlining will turn it into the appropriate formula
        // create invocation
        InvocationFormula inv = new InvocationFormula(new EmptyExpr(),
                                                      (QualifiedName)function_.getName().copy(),
                                                      (Exprs)varExprs.copy());
        inv.setVarTypeMapping(new HashMap());
        inv.setInvocable(function_);
        FormulaSeq newBody = new FormulaSeq((Formula)inv.copy());
        newBody.annotateTransformReplacing("desugaring of recursive function body",
                                           function_.getFormula());
        function_.setFormula(newBody);
    } // _addRelationFact
    **/
    /**
    private boolean _needsWrapper(InvocablePara function_, int index_) {
        if (!_funToWrapIndices.containsKey(function_)) return false;
        return ((Set)_funToWrapIndices.get(function_)).contains(new Integer(index_));
    }
    **/
    /**
    private SetMultExpr _wrapperSigSetMultExpr(SigType wrappedType_) {
        Signature sig = wrappedType_.getSignature();
        Signature wrapperSig = (Signature)_sigToWrapper.get(sig);
        Expr wrapSigExpr = wrapperSig.toSigExpr();
        SetMultExpr sme = new SetMultExpr(new SetMultiplicity(SetMultiplicity.NONE),
                                          wrapSigExpr);
        sme.setType(wrapSigExpr.getType());
        return sme;
    }
    **/
}
